T, T':Type, x:Id, c:T, a:Id, P:(TT'Prop).
T'
 (u:T. Dec(v:T'. P(u,v)))
 AtomFree(Type;T)
 AtomFree(Type;T')
 Feasible(ma-single-pre-init1(x;T;c;a;T';x,v.P(x,v))) 

latex

Definitions

x:A. B(x), Prop, P  Q, x:A. B(x), x(s1,s2), Feasible(M), ma-single-pre-init1(x;T;c;a;T';y,v.P(y;v)), with ds: ds init: initaction a:T precondition a(v) is P, x : v, mk-ma, , P & Q, xdom(f). v=f(x)   P(x;v), 1of(t), 2of(t), f(x)?z, ma-frame-compat(A;B), b, x  dom(f), f(x), if b t else f fi, M.rframe(A.pre p for a), M.frame(k affects x), M.aframe(k affects x), M.rframe(A.effect f of k on y), M.sframe(k sends <l,tg>), M.rframe(A.sends tfL of k on l), deq-member(eq;x;L), z != f(x)  P(a;z), reduce(f;k;as), false, Y, t  T, Dec(P), P  Q, true, P  Q, True, P  Q, b, T, Top, x. t(x), False, , Unit, State(ds), A, x(s),

Lemmas

assert wf, bor wf, eqof wf, id-deq wf, bfalse wf, Knd wf, Kind-deq wf, locl wf, ma-state wf, false wf, IdLnk wf, atom-free wf, decidable wf, Id wf, not wf, bool wf, iff transitivity, eqtt to assert, assert of bor, band wf, bnot wf, btrue wf, true wf, eqff to assert, squash wf, bnot thru bor, assert of band, and functionality wrt iff, assert of bnot, fpf-cap-single1, subtype rel self, deq property, fpf-single wf